Nuprl Lemma : eq_id_wf
0,22
postcript
pdf
a
,
b
:Id.
a
=
b
latex
Definitions
Id
,
t
T
,
IdDeq
,
x
:
A
.
B
(
x
)
,
eqof(
d
)
,
a
=
b
Lemmas
eqof
wf
,
id-deq
wf
,
Id
wf
origin
a, b:Id. a = b 
a, b:Id. a = b Tx:A. B(x)